minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
EQUAL2(s1(x), s1(y)) -> EQUAL2(x, y)
MIN2(s1(u), s1(v)) -> MIN2(u, v)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
MINUS2(x, y) -> EQUAL2(min2(x, y), y)
MINUS2(x, y) -> MIN2(x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
EQUAL2(s1(x), s1(y)) -> EQUAL2(x, y)
MIN2(s1(u), s1(v)) -> MIN2(u, v)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
MINUS2(x, y) -> EQUAL2(min2(x, y), y)
MINUS2(x, y) -> MIN2(x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
EQUAL2(s1(x), s1(y)) -> EQUAL2(x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
EQUAL2(s1(x), s1(y)) -> EQUAL2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
EQUAL2(s1(x), s1(y)) -> EQUAL2(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN2(s1(u), s1(v)) -> MIN2(u, v)
minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN2(s1(u), s1(v)) -> MIN2(u, v)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
MIN2(s1(u), s1(v)) -> MIN2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(equal2(min2(x, y), y), x, y)
cond3(true, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
minus2(x0, x1)
cond3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
MINUS2(0, x0) -> COND3(equal2(0, x0), 0, x0)
MINUS2(x0, 0) -> COND3(equal2(0, 0), x0, 0)
MINUS2(s1(x0), s1(x1)) -> COND3(equal2(s1(min2(x0, x1)), s1(x1)), s1(x0), s1(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
MINUS2(x0, 0) -> COND3(equal2(0, 0), x0, 0)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(0, x0) -> COND3(equal2(0, x0), 0, x0)
MINUS2(s1(x0), s1(x1)) -> COND3(equal2(s1(min2(x0, x1)), s1(x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(0, x0) -> COND3(equal2(0, x0), 0, x0)
MINUS2(s1(x0), s1(x1)) -> COND3(equal2(s1(min2(x0, x1)), s1(x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
MINUS2(0, s1(x0)) -> COND3(false, 0, s1(x0))
MINUS2(0, 0) -> COND3(true, 0, 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(0, s1(x0)) -> COND3(false, 0, s1(x0))
MINUS2(0, 0) -> COND3(true, 0, 0)
MINUS2(s1(x0), s1(x1)) -> COND3(equal2(s1(min2(x0, x1)), s1(x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), s1(x1)) -> COND3(equal2(s1(min2(x0, x1)), s1(x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ UsableRulesProof
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
MINUS2(s1(x0), s1(x1)) -> COND3(equal2(s1(min2(x0, x1)), s1(x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
MINUS2(s1(z0), s1(s1(z1))) -> COND3(equal2(s1(min2(z0, s1(z1))), s1(s1(z1))), s1(z0), s1(s1(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
MINUS2(s1(z0), s1(s1(z1))) -> COND3(equal2(s1(min2(z0, s1(z1))), s1(s1(z1))), s1(z0), s1(s1(z1)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
minus2(x0, x1)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
cond3(true, x0, x1)
equal2(0, s1(x0))
minus2(x0, x1)
cond3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(equal2(min2(x, y), y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
equal2(0, 0) -> true
equal2(s1(x), 0) -> false
equal2(0, s1(y)) -> false
equal2(s1(x), s1(y)) -> equal2(x, y)
min2(s1(x0), s1(x1))
equal2(s1(x0), 0)
equal2(0, 0)
min2(x0, 0)
equal2(s1(x0), s1(x1))
min2(0, x0)
equal2(0, s1(x0))